Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Spec] Added more specs to the coin and account modules #5832

Merged
merged 1 commit into from
Jan 4, 2023
Merged

[Spec] Added more specs to the coin and account modules #5832

merged 1 commit into from
Jan 4, 2023

Conversation

junkil-park
Copy link
Contributor

Description

  • this PR completes many TODOs in the specs of coin and account modules.
  • added more specs and helper spec functions to ed25519 and multi_ed25519 modules
  • enhanced the spec of type_info module
    • TODO: the spec of chain_id() is blocked by the bit operation support.

Test Plan

move prove

meng-xu-cs
meng-xu-cs reviewed Dec 10, 2022
View reviewed changes
Copy link
Collaborator

@meng-xu-cs meng-xu-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Leaving the ed25519 spec to crypto experts, the rest looks good to me.

aptos-move/framework/aptos-framework/sources/coin.spec.move Outdated Show resolved Hide resolved
alinush
alinush previously requested changes Dec 13, 2022
View reviewed changes
Copy link
Contributor

@alinush alinush left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we make the specs more modular? (see comments)

@junkil-park junkil-park force-pushed the jpark/spec-account branch 2 times, most recently from 2db36f0 to ac4cff9 Compare December 14, 2022 01:53
@junkil-park junkil-park enabled auto-merge (squash) January 4, 2023 02:57
@junkil-park
[Spec] Added more specs to the coin and account modules
140494c 
- this PR completes many TODOs in the specs of coin and account modules.
@github-actions

This comment has been minimized.

Sign in to view
@github-actions

This comment has been minimized.

Sign in to view
@github-actions
Copy link
Contributor

github-actions bot commented Jan 4, 2023

✅ Forge suite compat success on testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 140494c7414ac019d92ca213b8a4960db6933c19

Compatibility test results for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 140494c7414ac019d92ca213b8a4960db6933c19 (PR)
1. Check liveness of validators at old version: testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b
compatibility::simple-validator-upgrade::liveness-check : 7355 TPS, 5491 ms latency, 7700 ms p99 latency,no expired txns
2. Upgrading first Validator to new version: 140494c7414ac019d92ca213b8a4960db6933c19
compatibility::simple-validator-upgrade::single-validator-upgrade : 4532 TPS, 8759 ms latency, 11500 ms p99 latency,no expired txns
3. Upgrading rest of first batch to new version: 140494c7414ac019d92ca213b8a4960db6933c19
compatibility::simple-validator-upgrade::half-validator-upgrade : 5042 TPS, 8222 ms latency, 10900 ms p99 latency,no expired txns
4. upgrading second batch to new version: 140494c7414ac019d92ca213b8a4960db6933c19
compatibility::simple-validator-upgrade::rest-validator-upgrade : 6453 TPS, 5883 ms latency, 10000 ms p99 latency,no expired txns
5. check swarm health
Compatibility test for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 140494c7414ac019d92ca213b8a4960db6933c19 passed
Test Ok

@github-actions
Copy link
Contributor

github-actions bot commented Jan 4, 2023

✅ Forge suite land_blocking success on 140494c7414ac019d92ca213b8a4960db6933c19

performance benchmark with full nodes : 6640 TPS, 5988 ms latency, 10500 ms p99 latency,no expired txns
Test Ok

@junkil-park junkil-park dismissed alinush’s stale review January 4, 2023 05:04

Alin, I've addressed your comment making the spec more modular. I will move forward and land this for now to unblock the other spec work. However, please let me know if you have a further comment on this. I will be happy to re-iterate it. Thank you so much!

@junkil-park junkil-park merged commit 2743b5d into main Jan 4, 2023
@junkil-park junkil-park deleted the jpark/spec-account branch January 4, 2023 05:04
@Abuchtela Abuchtela mentioned this pull request Oct 27, 2023
Closed
@MuMianliu MuMianliu mentioned this pull request Oct 28, 2023
Open
@St0nersdash St0nersdash mentioned this pull request Oct 28, 2023
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@movekevin movekevin movekevin approved these changes

@rahxephon89 rahxephon89 rahxephon89 approved these changes

@davidiw davidiw Awaiting requested review from davidiw davidiw is a code owner

@wrwg wrwg Awaiting requested review from wrwg wrwg is a code owner

@alinush alinush Awaiting requested review from alinush

@meng-xu-cs meng-xu-cs Awaiting requested review from meng-xu-cs

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@junkil-park @alinush @rahxephon89 @meng-xu-cs @movekevin